Inference at * 1 3 1 0 2 
Iof proof for Lemma fincr wf:



1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
3. n : 
4. zz, n:. (n < zz)  (P(n))
  P(n) 

latex

 by (\p.let i = mvt (var_of_hyp (-2) p) in 
 blet ip1 = mk_add_term  i 1 in 
 b((DTerm ip1 (-1))

CollapseTHENM (DTerm i (-1))) p) 

latex

C1: .....wf..... NILNIL

C1: 3. n : 
C1:   n+1  
C2: .....wf..... NILNIL

C2: 3. n : 
C2:   n  
C3: 

C3: 4. (n < (n+1))  (P(n))
C3:   P(n)
C.

Definitions

#$n, n+m, s = t, f(a), a < b, P  Q, , , x:AB(x), x:A. B(x), t  T